; -- capstoneDriver.lisp, a program fragment for the capstone project --

; WARNING! You must use this file exactly as is, except for inserting
;          your source code where the comments call for it.

;;----------------------------------------------------------------------------
;;
;;           Team Hoare
;;          
;;           Bryan Gilcrease
;;           Ryan Keith
;;           Michael Riggs
;;           Michael Young
;;           Stanton White
;;
;;-----------------------------------------------------------------------------

(include-book "world" :dir :teachpacks)
(include-book "io-utilities" :dir :teachpacks)

;;
;;Updated AVL CODE
;;
; Extractors (and empty-tree detector)
(defun empty-tree? (tr) (not (consp tr)))
(defun height (tr) (if (empty-tree? tr) 0 (car tr)))
(defun key (tr) (cadr tr))
(defun data (tr) (caddr tr))
(defun left (tr) (cadddr tr))
(defun right (tr) (car (cddddr tr)))
(defun keys (tr)
  (if (empty-tree? tr)
      nil
      (append (keys (left tr)) (list (key tr)) (keys (right tr)))))

; Constructors
(defun empty-tree ( ) nil)
(defun tree (k d lf rt)
		(list (+ 1 (max (height lf) (height rt))) k d lf rt))

; Contstraint detectors and key comparators
(defun key? (k) (rationalp k))	  ; to change representation of keys
(defun key< (j k) (< j k))	  ;     alter definitions of key? and key<
(defun key> (j k) (key< k j))
(defun key= (j k)		  ; note: definitions of
  (and (not (key< j k))           ;    key>, key=, and key-member	
       (not (key> j k))))	  ;        get in line automatically
(defun key-member (k ks)
  (and (consp ks)
       (or (key= k (car ks))
           (key-member k (cdr ks)))))
(defun data? (d)
  (if d t t))
(defun tree? (tr)
  (or (empty-tree? tr)
      (and (natp (height tr))		       ; height
           (= (height tr)                      ;   constraints
              (+ 1 (max (height (left tr))
                        (height (right tr)))))
           (key? (key tr))                     ; key constraint
           (data? (data tr))                   ; data constraint
           (tree? (left tr))                   ; subtree
           (tree? (right tr)))))               ;   constraints

; Key occurs in tree detector
(defun occurs-in-tree? (k tr)
  (and (key? k)
       (tree? tr)
       (key-member k (keys tr))))
(defun alternate-occurs-in-tree? (k tr)
  (and (key? k)
       (tree? tr)
       (not (empty-tree? tr))
       (or (key= k (key tr))
           (alternate-occurs-in-tree? k (left tr))
           (alternate-occurs-in-tree? k (right tr)))))

; all-key comparators
(defun all-keys< (k ks)
  (or (not (consp ks))
      (and (key< (car ks) k) (all-keys< k (cdr ks)))))

(defun all-keys> (k ks)
  (or (not (consp ks))
      (and (key> (car ks) k) (all-keys> k (cdr ks)))))

; definitions of ordered and balanced, and avl-tree detector
(defun ordered? (tr)
  (or (empty-tree? tr)
      (and (tree? tr)
           (all-keys< (key tr) (keys (left tr)))
           (all-keys> (key tr) (keys (right tr)))
           (ordered? (left tr))
           (ordered? (right tr)))))

(defun balanced? (tr)
  (and (tree? tr)
       (or (empty-tree? tr)
           (and (<= (abs (- (height (left tr)) (height (right tr)))) 1)
           (balanced? (left tr))
           (balanced? (right tr))))))

(defun avl-tree? (tr)
  (and (ordered? tr)
       (balanced? tr)))

; rotations
(defun easy-R (tr)
  (let* ((z (key tr)) (dz (data tr))
         (zL (left tr)) (zR (right tr))
         (x (key zL)) (dx (data zL))
         (xL (left zL)) (xR (right zL)))
     (tree x dx xL (tree z dz xR zR))))

(defun easy-L (tr)
  (let* ((z (key tr)) (dz (data tr))
         (zL (left tr)) (zR (right tr))
         (x (key zR)) (dx (data zR))
         (xL (left zR)) (xR (right zR)))
     (tree x dx (tree z dz zL xL) xR)))

(defun left-heavy? (tr)
  (and (tree? tr)
       (not (empty-tree? tr))
       (= (height (left tr)) (+ 2 (height (right tr))))))

(defun outside-left-heavy? (tr)
  (and (left-heavy? tr)
       (or (= (height (left (left tr)))
              (height (right (left tr))))
           (= (height (left (left tr)))
              (+ 1 (height (right (left tr))))))))

(defun right-rotatable? (tr)
  (and (ordered? tr)
       (not (empty-tree? tr))
       (balanced? (left tr))
       (balanced? (right tr))
       (not (empty-tree? (left tr)))))

(defun right-heavy? (tr)
  (and (tree? tr)
       (not (empty-tree? tr))
       (= (height (right tr)) (+ 2 (height (left tr))))))

(defun outside-right-heavy? (tr)
  (and (right-heavy? tr)
       (or (= (height (right (right tr))) (height (left (right tr))))
           (= (height (right (right tr))) (+ 1 (height (left (right tr))))))))

(defun left-rotatable? (tr)
  (and (tree? tr)
       (not (empty-tree? tr))
       (balanced? (left tr))
       (balanced? (right tr))
       (not (empty-tree? (right tr)))))

(defun hard-R (tr)
  (let* ((z (key tr))
         (dz (data tr))
         (zL (left tr))
         (zR (right tr)))
     (easy-R (tree z dz (easy-L zL) zR))))

(defun hard-L (tr)
  (let* ((z (key tr))
         (dz (data tr))
         (zL (left tr))
         (zR (right tr)))
     (easy-L (tree z dz zL (easy-R zR)))))

(defun inside-left-heavy? (tr)
  (and (left-heavy? tr)
       (= (height (right (left tr)))
          (+ 1 (height (left (left tr)))))))

(defun hard-R-rotatable? (tr)
  (and (right-rotatable? tr)
       (left-rotatable? (left tr))))

(defun inside-right-heavy? (tr)
  (and (right-heavy? tr)
       (= (height (left (right tr)))
          (+ 1 (height (right (right tr)))))))

(defun hard-L-rotatable? (tr)
  (and (left-rotatable? tr)
       (right-rotatable? (right tr))))

(defun rot-R (tr)
  (let ((zL (left tr)))
     (if (< (height (left zL)) (height (right zL)))
         (hard-R tr)
         (easy-R tr))))

(defun rot-L (tr)
  (let ((zR (right tr)))
     (if (< (height (right zR)) (height (left zR)))
         (hard-L tr)
         (easy-L tr))))

; insertion
(defun avl-insert (tr new-key new-datum)
  (if (empty-tree? tr)
      (tree new-key new-datum (empty-tree) (empty-tree))
      (if (key< new-key (key tr))
          (let* ((subL (avl-insert (left tr) new-key new-datum))
                 (subR (right tr))
                 (new-tr (tree (key tr) (data tr) subL subR)))
             (if (= (height subL) (+ (height subR) 2))
                 (rot-R new-tr)
                        new-tr))
          (if (key> new-key (key tr))
              (let* ((subL (left tr))
                     (subR (avl-insert (right tr) new-key new-datum))
                     (new-tr (tree (key tr) (data tr) subL subR)))
                 (if (= (height subR) (+ (height subL) 2))
                     (rot-L new-tr)
                     new-tr))
              (tree new-key new-datum (left tr) (right tr))))))

; delete root - easy case
(defun easy-delete (tr)
  (right tr))

; tree shrinking
(defun shrink (tr)
  (if (empty-tree? (right tr))
      (list (key tr) (data tr) (left tr))
      (let* ((key-data-tree (shrink (right tr)))
             (k (car key-data-tree))
             (d (cadr key-data-tree))
             (subL (left tr))
             (subR (caddr key-data-tree))
             (shrunken-tr (tree (key tr) (data tr) subL subR)))
         (if (= (height subL) (+ 2 (height subR)))
             (list k d (rot-R shrunken-tr))
             (list k d shrunken-tr)))))

(defun raise-sacrum (tr)
   (let* ((key-data-tree (shrink (left tr)))
          (k (car key-data-tree))
          (d (cadr key-data-tree))
          (subL (caddr key-data-tree))
          (subR (right tr))
          (new-tr (tree k d subL subR)))
     (if (= (height subR) (+ 2 (height subL)))
         (rot-L new-tr)
         new-tr)))

; delete root - hard case
(defun delete-root (tr)
  (if (empty-tree? (left tr))
      (easy-delete tr)
      (raise-sacrum tr)))

; deletion
(defun avl-delete (tr k)
  (if (empty-tree? tr)
      tr
      (if (key< k (key tr))           ; key occurs in left subtree
          (let* ((new-left (avl-delete (left tr) k))
                 (new-tr (tree (key tr) (data tr) new-left (right tr))))
             (if (= (height (right new-tr)) (+ 2 (height (left new-tr))))
                 (rot-L new-tr)
                 new-tr))
          (if (key> k (key tr))       ; key occurs in right subtree
              (let* ((new-right (avl-delete (right tr) k))
                     (new-tr (tree (key tr) (data tr) (left tr) new-right)))
                     (if (= (height (left new-tr)) (+ 2 (height (right new-tr))))
                         (rot-R new-tr)
                         new-tr))
                 (delete-root tr)))))  ; key occurs at root

; retrieval
(defun avl-retrieve (tr k)  ; delivers key/data pair with key = k
  (if (empty-tree? tr)      ; or nil if k does not occur in tr
      nil                                 ; signal k not present in tree
      (if (key< k (key tr))
          (avl-retrieve (left tr) k)      ; search left subtree
          (if (key> k (key tr))
              (avl-retrieve (right tr) k) ; search right subtree
              (cons k (data tr))))))      ; k is at root, deliver key/data pair

(defun avl-flatten (tr)  ; delivers all key/data cons-pairs
  (if (empty-tree? tr)   ; with keys in increasing order
      nil
      (append (avl-flatten (left tr))
              (list (cons (key tr) (data tr)))
              (avl-flatten (right tr)))))

(defun occurs-in-pairs? (k pairs)
  (and (consp pairs)
       (or (key= k (caar pairs))
           (occurs-in-pairs? k (cdr pairs)))))

(defun increasing-pairs? (pairs)
  (or (not (consp (cdr pairs)))
      (and (key< (caar pairs) (caadr pairs))
           (increasing-pairs? (cdr pairs)))))
;;
;;END OF AVL CODE
;;

;; Alive-Cells Abstract Data Type
(defun alive-cells? (ac)
  (avl-tree? ac))

(defun alive-cells-constructor ()
  (empty-tree))

(defun alive-cells-insert (ac cell-id)
  (avl-insert ac cell-id 1))

(defun alive-cells-retrieve (ac cell-id)
  (avl-retrieve ac cell-id))

(defun alive-cells-kill (ac cell-id)
  (avl-delete ac cell-id))

(defun alive-cells-list (ac)
   (strip-cars (avl-flatten ac)))

(defun debug-output (crap)
  (+ crap 1))

;; Dead-Neighbors Abstract Data Type
(defun dead-neighbors-constructor ()
  (empty-tree))

(defun dead-neighbors-insert (x dn)
  (let ((previous (avl-retrieve dn x)))
    (if (consp previous)
        (avl-insert dn x (1+ (cdr previous)))
        (avl-insert dn x 1))))

(defun dead-neighbors-insert-list (lst dn)
  (if (endp lst)
      dn
      (dead-neighbors-insert (car lst) (dead-neighbors-insert-list (cdr lst) dn))))

; Returns a list of cons pairs, with the first number being the cell-id and
; the second number being the number of times it occurred.
(defun dead-neighbors-list (dn)
  (avl-flatten dn))
            
; ----- NEIGHBOR FUNCTIONS START -----
(defconst *BOARD-WIDTH* 30)
(defconst *BOARD-HEIGHT* 30)
;; For the Honeycomb topology there are two widths
;; every other row is one cell longer
;; *HC-BOARD-WIDTH* is the longer of the two
(defconst *HC-BOARD-WIDTH* 21)
(defconst *BOARD-MAX-ID* (- (* *BOARD-WIDTH* *BOARD-HEIGHT*) 1))

(defun cell-in-range? (cell-id dimension)
  (and (natp cell-id)
       (>= cell-id 0) 
       (<= cell-id (+ (- (* dimension dimension) 1) 1))))

;;calculation for computing the neighbors of the edges on
;;the moebius-strip and klein-bottle
(defun moebius-klein-neighbor (cell-id dimension)
  (+ (- (+ (- (* dimension dimension) 1) 1) cell-id) 1))

;;if the cell is on the edge this function finds the topo
;;specific neighbor
(defun get-topo-top-neighbor (cell-id topo dimension)
  (case topo
    ('Cylinder nil)
    ('Moebius nil)
    ('Torus (+ cell-id (* dimension (- dimension 1))))
    ('Klein (moebius-klein-neighbor cell-id dimension)))) 

(defun get-top-neighbor (cell-id topo dimension)
  (if (not (and (natp cell-id)
	        (cell-in-range? cell-id dimension)))
    nil
    (if (not (> cell-id dimension))
      (get-topo-top-neighbor cell-id topo dimension)
      (- cell-id dimension))))
  
;;if the cell is on the edge this function finds the topo
;;specific neighbor
(defun get-topo-bottom-neighbor (cell-id topo dimension)
  (case topo
    ('Cylinder nil)
    ('Moebius nil) 
    ('Torus (- cell-id (* dimension (- dimension 1))))
    ('Klein (moebius-klein-neighbor cell-id dimension))))

(defun get-bottom-neighbor (cell-id topo dimension)
  (if (not (and (natp cell-id)
	        (cell-in-range? cell-id dimension)))
    nil
    (if (> cell-id (* dimension (- dimension 1))) 
      (get-topo-bottom-neighbor cell-id topo dimension)
      (+ cell-id dimension))))
  

;;if the cell is on the edge this function finds the topo
;;specific neighbor
(defun get-topo-left-neighbor (cell-id topo dimension)
  (case topo
    ('Cylinder (+ cell-id (- dimension 1)))
    ('Moebius (moebius-klein-neighbor cell-id dimension))
    ('Torus (+ cell-id (- dimension 1)))
    ('Honeycomb nil)
    ('Klein (moebius-klein-neighbor cell-id dimension)))) 

(defun get-left-neighbor (cell-id topo dimension)
  (if (not (and (natp cell-id)
	        (cell-in-range? cell-id dimension)))
    nil
    (if (not (= (mod cell-id dimension) 1)) 
      (- cell-id 1)
      (get-topo-left-neighbor cell-id topo dimension))))

;;if the cell is on the edge this function finds the topo
;;specific neighbor
(defun get-topo-right-neighbor (cell-id topo dimension)
  (case topo
    ('Cylinder (- cell-id (- dimension 1)))
    ('Moebius (moebius-klein-neighbor cell-id dimension)) 
    ('Torus (- cell-id (- dimension 1)))
    ('Honeycomb nil)
    ('Klein (moebius-klein-neighbor cell-id dimension))))

(defun get-right-neighbor (cell-id topo dimension)
  (if (not (and (natp cell-id)
	        (cell-in-range? cell-id dimension)))
    nil
    (if (<= (mod cell-id dimension) 0) 
      (get-topo-right-neighbor cell-id topo dimension)
      (+ cell-id 1))))

(defun get-top-left-neighbor (cell-id topo dimension)
  (get-left-neighbor (get-top-neighbor cell-id topo dimension) topo dimension))

(defun get-hc-top-left-neighbor (cell-id dimension)
  (if (and (cell-in-range? cell-id dimension)
	   (> cell-id dimension))
    (- cell-id (+ (mod (floor cell-id dimension) 2) dimension))
    nil))

(defun get-top-right-neighbor (cell-id topo dimension)
  (get-right-neighbor (get-top-neighbor cell-id topo dimension) topo dimension))

(defun get-hc-top-right-neighbor (cell-id dimension)
  (if (and (cell-in-range? cell-id dimension)
	   (> cell-id dimension))
    (- cell-id (+ (mod (floor cell-id dimension) 2) (- dimension 1)))
    nil))

(defun get-bottom-left-neighbor (cell-id topo dimension)
  (get-left-neighbor (get-bottom-neighbor cell-id topo dimension) topo dimension))

(defun get-hc-bottom-left-neighbor (cell-id dimension)
  (if (and (cell-in-range? cell-id dimension)
	   (< cell-id (- (- (* dimension dimension) 1) dimension)))
    (+ cell-id (- dimension (mod (floor cell-id dimension) 2)))
    nil))

(defun get-bottom-right-neighbor (cell-id topo dimension)
  (get-right-neighbor (get-bottom-neighbor cell-id topo dimension) topo dimension))

(defun get-hc-bottom-right-neighbor (cell-id dimension)
  (if (and (cell-in-range? cell-id dimension)
	   (< cell-id (- (- (* dimension dimension) 1) dimension)))
    (+ cell-id (+ dimension (- 1 (mod (floor cell-id dimension) 2))))
    nil))

; returns a list of the cell's neighbors
(defun neighbor-list (cell-id topo dimension)
  (if (eq topo 'Honeycomb)
    (remove nil 
      (cons (get-hc-top-right-neighbor cell-id dimension)
        (cons (get-right-neighbor cell-id topo dimension)
          (cons (get-hc-bottom-right-neighbor cell-id dimension)
             (cons (get-hc-bottom-left-neighbor cell-id dimension)
                (cons (get-left-neighbor cell-id topo dimension)
                  (cons (get-hc-top-left-neighbor cell-id dimension)
	            nil)))))))
    (remove nil 
      (cons (get-top-neighbor cell-id topo dimension)
        (cons (get-top-right-neighbor cell-id topo dimension)
          (cons (get-right-neighbor cell-id topo dimension)
            (cons (get-bottom-right-neighbor cell-id topo dimension)
              (cons (get-bottom-neighbor cell-id topo dimension)
                (cons (get-bottom-left-neighbor cell-id topo dimension)
                  (cons (get-left-neighbor cell-id topo dimension)
                    (cons (get-top-left-neighbor cell-id topo dimension)
                       nil)))))))))))

; ----- NEIGHBOR FUNCTIONS END -----


; ----- TREE UPDATE FUNCTIONS START -----
; In general:
; t   = life
; nil = death

; Checks the tree for the cell-id
; returns t if found, nil if not found
(defun alive? (cell-id alive-cells)
  (if (alive-cells-retrieve alive-cells cell-id)
      t
      nil))

; Takes in neighbors of an alive cell and checks if cell needs to die, 
; and also adds all of its dead
; neighbors to a list.
; returns t if cell can stay alive, nil if it needs to die
; returns a list of dead neighbors
(defun check-neighbors (neighbors dead-neighbors num-alive-neighbors ac)
  (if (endp neighbors)
      (if (and (< num-alive-neighbors 4) (> num-alive-neighbors 1))
          (mv t dead-neighbors)    ; I can stay alive.
          (mv nil dead-neighbors)) ; I'm dead.          
      (if (alive? (car neighbors) ac)
          (check-neighbors (cdr neighbors) dead-neighbors 
                           (1+ num-alive-neighbors) ac)
          (check-neighbors (cdr neighbors) (cons (car neighbors) dead-neighbors) 
                           num-alive-neighbors ac))))

; Checks one alive cell.
; returns cell-id if the cell needs to die or nil if it should stay alive
; returns a list of dead neighbors adjacent to the cell
(defun check-alive-cell (cell-id topo ac dimension)
  (mv-let (stay-alive? dead-neighbors)
          (check-neighbors (neighbor-list cell-id topo dimension) nil 0 ac)
          (if stay-alive?
              (mv nil dead-neighbors)
              (mv cell-id dead-neighbors))))

; Check all alive cells in the tree.
; returns a list of cell-ids to kill
; returns a list of dead cell-ids which neighbor alive cells
(defun check-alive-cells (ac-list topo ac dimension)
  (if (endp ac-list)
      (mv nil (dead-neighbors-constructor)) 
      (mv-let (need-to-die-cell-id-car dead-neighbors-car)
              (check-alive-cell (car ac-list) topo ac dimension)
              (mv-let (need-to-die-cell-id-cdr dead-neighbors-cdr)
                      (check-alive-cells (cdr ac-list) topo ac dimension)
                      (mv (remove nil (cons need-to-die-cell-id-car 
                                            need-to-die-cell-id-cdr))
                          (dead-neighbors-insert-list dead-neighbors-car
                                                      dead-neighbors-cdr))))))

; Check an individual dead neighbor
; returns t if cells needs to be revived, or nil if the cell needs to stay dead
;(defun check-dead-neighbors-neighbors (dead-neighbor 
;                      neighbors-list num-alive-neighbors ac)
;  (if (endp neighbors-list)
;      (if (= num-alive-neighbors 3)
;          dead-neighbor ; revive me
;          nil) ; stay dead
;      (if (alive? (car neighbors-list) ac)
;          (check-dead-neighbors-neighbors dead-neighbor 
;                                          (cdr neighbors-list)
;                                          (1+ num-alive-neighbors) ac)
;          (check-dead-neighbors-neighbors dead-neighbor 
;                                          (cdr neighbors-list)
;                                          num-alive-neighbors ac))))

; Checks dead neighbors to determine if any need to be revived.
; returns a list of cell-ids that need to be revived
(defun check-dead-neighbors (dn)
  (if (endp dn)
      nil
      (let ((cell-id (car (car dn)))
            (num-alive-neighbors (cdr (car dn))))
        (if (= num-alive-neighbors 3)
            (cons cell-id (check-dead-neighbors (cdr dn)))
            (check-dead-neighbors (cdr dn))))))

; Removes cells in the kill-list from the tree.
; returns an updated tree
(defun kill-cells (kill-list ac)
  (if (endp kill-list)
      ac
      (kill-cells (cdr kill-list) (alive-cells-kill ac (car kill-list)))))

; Adds cells in the revive-list to the tree.
; returns an updated tree
(defun revive-cells (revive-list ac)
  (if (endp revive-list)
      ac
      (revive-cells (cdr revive-list) 
                    (alive-cells-insert ac (car revive-list)))))

; Master Update Function
; returns an updated tree
(defun update-tree (ac topo dimension)
  (mv-let (kill-list dead-neighbors)
          (check-alive-cells (alive-cells-list ac) topo ac dimension)
          (let ((revive-list (check-dead-neighbors (dead-neighbors-list
                                                    dead-neighbors))))
            (revive-cells revive-list (kill-cells kill-list ac)))))

; ----- TREE UPDATE FUNCTIONS END -----

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;             MERGE-SORT FUNCTIONS                                      ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun ordered-p (lst)
  (or (endp lst)
      (endp (cdr lst))
      (and (<= (car lst) (car (cdr lst)))
           (ordered-p (cdr lst)))))

(defun delete-element (a lst)
  (if (endp lst)
      lst
    (if (equal a (car lst))
        (cdr lst)
      (cons (car lst) (delete-element a (cdr lst))))))

(defun permutation-p (left right)
  (or (and (endp left) (endp right))
      (and (consp left)
           (member (car left) right)
           (permutation-p (cdr left) (delete-element (car left) right)))))

;; Merge function for merge-sort
(defun merge-results(left right)
  (declare (xargs :measure (+ (length left)(length right))))
  (if (and (true-listp left)(true-listp right))
      (if (and (consp left)(consp right))
          (if (<= (car left)
                  (car right))
              (cons (car left)
                    (merge-results (cdr left) right))
              (cons (car right)
                    (merge-results left (cdr right))))
          (if (consp left)
              left
              right))
      nil))

;; Merge function for merge-sort-by-time function
(defun merge-by-time (left right)
  (declare (xargs :measure (+ (length left)(length right))))
  (if (and (true-listp left)(true-listp right))
      (if (and (consp left)(consp right))
          (let* ((timel (car (car left))) ;get left timestamp
                 (timer (car (car right)))) ;get right timestamp
            (if (<= timel timer) ;if timestamp of left <= timestamp of right
                (cons (car left)
                      (merge-by-time (cdr left) right))
                (cons (car right) ;else
                      (merge-by-time left(cdr right)))))
            (if (consp left) ;cleanup the rest
                left
                right))
          nil))

; delivers every other element of the list xs, starting with the first
(defun every-other (xs)
  (if (consp xs)
      (cons (car xs) (every-other (cddr xs)))
      nil))

; delivers every other element of the list xs, starting with the second
(defun every-odd (xs)
  (if (consp (cdr xs))
      (cons (cadr xs) (every-odd (cddr xs)))
      nil))

;; The new list is smaller than the original (needed for the admission of
;; the merge-sort functions).
(defthm every-other-is-smaller
  (implies (and (consp xs) (consp (cdr xs)))
           (< (acl2-count (every-other xs))
              (acl2-count xs))))

;; The new list is smaller than the original (needed for the admission of
;; the merge-sort functions).
(defthm every-odd-is-smaller
  (implies (and (consp xs)(consp (cdr xs)))
           (< (acl2-count (every-odd xs))
              (acl2-count xs))))

;; Used by merge-sort to split the given list into two lists, where
;; one list contains every "odd-indexed" element and the other contains
;; every "even-indexed" element.
(defun split-list (x)
  (mv (every-other x)(every-odd x)))

;; O(n lg n) sorting function, sorts the given list alphabetically.
(defun merge-sort (x)
  (if (endp x)
      nil
      (if (endp (cdr x))
          x
	(mv-let (left right)
		(split-list x)
		(merge-results (merge-sort left) (merge-sort right))))))

;; O(n lg n) sorting function, sorts the given list according to the 
;; timesteps. xs must be a list of list of integers in which the first
;; number of each list is the timestep.
(defun merge-sort-by-time (xs)
  (if (endp xs)
      nil
      (if (endp (cdr xs))
          xs
          (mv-let (left right)
                  (split-list xs)
                  (merge-by-time (merge-sort-by-time left)
                                      (merge-sort-by-time right))))))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;             END MERGE-SORT FUNCTIONS                                  ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


; DESCRIPTION OF REQUIRED FUNCTIONS AND CONSTANTS
;   The datatype "world" specifies a representation of the state
;   of the world. You will design this datatype.
  
; Define functions and constants with the following signatures
;   world-image  : World -> Image           --responds to redraw events
;   world-next   : World -> World           --responds to time-step events
;   world-change : World KeyEvent -> World  --responds to keyboard events
;   *w-disp*    : nat      --width in pixels of display canvas
;   *h-disp*    : nat      --height in pixels of display canvas
;   *tick*      : rational --elapsed time in one time-step (in seconds)
;   *new-world* : world    --state of world before big bang
; END OF DESCRIPTION OF REQUIRED FUNCTIONS AND CONSTANTS

; PASTE YOUR SOURCE CODE HERE
(defconst *tick* 1/10)

; window width
(defconst *w-disp*  500)

; window height
(defconst *h-disp* 500)

; height of the grid within the window
(defconst *grid-height* 400)

; the number of cells in each row and column
(defconst *dimensions* 20)

; the width of each individual cell
(defconst *cell-width* (/ *w-disp* *dimensions*))

; the height of each individual cell
(defconst *cell-height* (/ *grid-height* *dimensions*))

; x-coordinate for each radio button
(defconst *radio-x* (+ (floor *w-disp* 3) 30))

; x-coordinate for each label for the radio buttons
(defconst *label-x* (+ *radio-x* 10))

; x coordinate for cylinder radio
(defconst *cylinder-radio-x* *radio-x*)

; y coordinate for cylinder radio
(defconst *cylinder-radio-y* (floor *grid-height* 3))

; x coordinate for cylinder radio label
(defconst *cylinder-label-x* *label-x*)

; y coordinate for cylinder radio label
(defconst *cylinder-label-y* (- *cylinder-radio-y* 8))

; x coordinate for moebius strip radio
(defconst *moebius-radio-x* *radio-x*)

; y coordinate for moebius strip radio button
(defconst *moebius-radio-y* (+ *cylinder-radio-y* 20));78))

; x coordinate for moebius strip radio label
(defconst *moebius-label-x* *label-x*)

; y coordinate for moebius strip radio label
(defconst *moebius-label-y* (- *moebius-radio-y* 8))

; x coordinate for torus radio button
(defconst *torus-radio-x* *radio-x*)

; y coordinate for torus radio button
(defconst *torus-radio-y* (+ *moebius-radio-y* 20));66))

; x coordinate for torus radio label
(defconst *torus-label-x* *label-x*)

; y coordinate for torus radio label
(defconst *torus-label-y* (- *torus-radio-y* 8))

; x coordinate for klein bottle radio button
(defconst *klein-radio-x* *radio-x*)

; y coordinate for klein bottle radio button
(defconst *klein-radio-y* (+ *torus-radio-y* 20));66))

; x coordinate for klein bottle radio label
(defconst *klein-label-x* *label-x*)

; y coordinate for klein bottle radio label
(defconst *klein-label-y* (- *klein-radio-y* 8))

; x coordinate for honeycomb radio button
(defconst *honeycomb-radio-x* *radio-x*)

; y coordinate for honeycomb radio button
(defconst *honeycomb-radio-y* (+ *klein-radio-y* 20));;234

; x coordinate for honeycomb radio label
(defconst *honeycomb-label-x* *label-x*)

; y coordinate for honeycomb radio label
(defconst *honeycomb-label-y* (- *honeycomb-radio-y* 8))

; y coordinate for game of life title on initial menu
(defconst *title-y* (- *cylinder-radio-y* 100))

; x coordinate for the "next" button on the initial menu
(defconst *next-button-x* *radio-x*)

; y coordinate for the "next" button on the initial menu
(defconst *next-button-y* (+ *klein-label-y* 50))

; width of the "next" button on the initial menu
(defconst *next-button-w* 65)

; height of the "next" button on the initial menu
(defconst *next-button-h* 22)

; x coordinate for the "next" button on the initial menu
(defconst *start-button-x* *radio-x*)

; y coordinate for the "next" button on the initial menu
(defconst *start-button-y* (+ *grid-height* 20))

; width of the "next" button on the initial menu
(defconst *start-button-w* 65)

; height of the "next" button on the initial menu
(defconst *start-button-h* 22)

; x coordinate for the "next" button on the initial menu
(defconst *pause-button-x* *radio-x*)

; y coordinate for the "next" button on the initial menu
(defconst *pause-button-y* (+ *grid-height* 20))

; width of the "next" button on the initial menu
(defconst *pause-button-w* 65)

; height of the "next" button on the initial menu
(defconst *pause-button-h* 22)

; x coordinate for the "next" button on the initial menu
(defconst *reset-button-x* (+ 5 (+ *pause-button-x* *pause-button-w*)))

; y coordinate for the "next" button on the initial menu
(defconst *reset-button-y* (+ *grid-height* 20))

; width of the "next" button on the initial menu
(defconst *reset-button-w* 65)

; height of the "next" button on the initial menu
(defconst *reset-button-h* 22)

; topology label x
(defconst *topo-label-x* (+ *reset-button-x* 170))

; topology label y
(defconst *topo-label-y* (+ *reset-button-y* 3))

; x coordinate for 20 x 20 size selector radio button
(defconst *size-radio-x-20* 40)

; x coordinate for 50 x 50 size selector button
(defconst *size-radio-x-50* *size-radio-x-20*)

; x coordinate for 100 x 100 size selector button
(defconst *size-radio-x-100* *size-radio-x-20*)

; y coordinate for 20 x 20 size selector button
(defconst *size-radio-y-20* (+ *grid-height* 27))

; y coordinate for 50 x 50 size selector button
(defconst *size-radio-y-50* (+ *size-radio-y-20* 20))

; y coordinate for 100 x 100 size selector button
(defconst *size-radio-y-100* (+ *size-radio-y-50* 20))

; x coordinate for 20 x 20 label
(defconst *size-label-x-20* (+ *size-radio-x-20* 20))

; x coordinate for 50 x 50 label
(defconst *size-label-x-50* (+ *size-radio-x-50* 20))

; x coordinate for 100 x 100 label
(defconst *size-label-x-100* (+ *size-radio-x-100* 20))

; y coordinate for 20 x 20 label
(defconst *size-label-y-20* (- *size-radio-y-20* 8))

; y coordinate for 50 x 50 label
(defconst *size-label-y-50* (+ *size-label-y-20* 20))

; y coordinate for 100 x 100 label
(defconst *size-label-y-100* (+ *size-label-y-50* 20))

; x-coordinate for "graph" button
(defconst *graph-button-x* *radio-x*)

; y-coordinate for "graph" button
(defconst *graph-button-y* (+ *grid-height* 50))

; width of graph button
(defconst *graph-button-w* 65)

; height of graph button
(defconst *graph-button-h* 22)

; leftmost x-coordinate of x-axis on population graph
(defconst *x-axis-x1* 30)

; rightmost x-coordinate of x-axis on population graph
(defconst *x-axis-x2* (- *w-disp* 30))

; span of the x-axis on the population graph
(defconst *x-axis-width* (- *x-axis-x2* *x-axis-x1*))

; y-coordinate of the x-axis on the population graph
(defconst *x-axis-y* (floor *h-disp* (/ 5 4)))

; number of tick marks on the x-axis
(defconst *x-tick-marks* 4)

; distance between tick marks on the x-axis
(defconst *x-tick-width* (floor *x-axis-width*
                              (+ *x-tick-marks* 1)))

; leftmost coordinate for "Time" label on x-axis
(defconst *x-axis-label-x* (floor (- *x-axis-x2* *x-axis-x1*) 2))

; y-coordinate of "Time" label on x-axis
(defconst *x-axis-label-y* (+ *x-axis-y* 50))

; leftmost coordinate of the graph title
(defconst *graph-title-x* (floor *w-disp* 4))

; y-coordinate of the graph title
(defconst *graph-title-y* 10)

; x-coordinate of the y-axis
(defconst *y-axis-x* *x-axis-x1*)

; bottomost y-coordinate of the y-axis
(defconst *y-axis-y1* *x-axis-y*)

; topmost y-coordinate of the y-axis
(defconst *y-axis-y2* 45)

; vertical span of the y-axis
(defconst *y-axis-height* (- *y-axis-y1* *y-axis-y2*))

; number of tick marks on the y-axis
(defconst *y-tick-marks* 4)

; distance between ticks on the y-axis
(defconst *y-tick-width* (floor *y-axis-height*
                                (+ *y-tick-marks* 1)))

(defconst *reset-button-x2* *x-axis-label-x*)

(defconst *reset-button-y2* (+ *x-axis-label-y* 20))

; the maximum number of points to collect for the population graph
(defconst *stats-limit* 100)

; default text size for the interface
(defconst *txt-size* 10)

; default text color for the interface
(defconst *txt-color* 'black)

; Constants indicating the phase of the sim for the interface
(defconst *initial-menu* 1)
(defconst *board-setup* 2)
(defconst *run-sim* 3)
(defconst *graph* 4)

; the world structure:
;    selected: the selected topology
;    phase: the current phase of the game (see above constants)
;    board: the tree of alive cells
;    population-sizes: list of populations gathered as the game runs
;    population-and-time: coordinate pairs of (time, population).
;    timestamp: the current time
;    size: the dimensions of the grid (20 = 20 x 20, 50 = 50 x 50,
;                                      100 = 100 x 100)
;    cursor-locations: a holdover from when keyboard input was allowed
(defstructure the-world 
  (selected (:assert (symbolp selected)))
  (phase (:assert (integerp phase)))
  (board (:assert (alive-cells? board)))
  (population-sizes (:assert (integer-listp population-sizes)))
  (population-and-time (:assert (true-list-listp population-and-time)))
  (timestamp (:assert (integerp timestamp)))
  (size (:assert (natp size)))
  (cursor-location (:assert (integerp cursor-location))))

; the initial world
(defconst *new-world* 
  (the-world 'Cylinder 1 (alive-cells-constructor) nil nil 1 20 1 ))

;; Function responsible for drawing the next button on the intial menu
;; Type: nil -> Image
(defun draw-button ()
  (let* ((border (rectangle (+ *next-button-w* 1)
                            (+ *next-button-h* 1)
                            'outline 
                            'black))
         (box (rectangle *next-button-w* *next-button-h* 'solid 'gray))
         (label (text "  Next >" *txt-size* 'white))
         (rect (overlay border box))
         (button (overlay rect label)))
    (place-image button
                 *next-button-x*
                 *next-button-y*
                 (empty-scene *w-disp* *h-disp*))))

;; Function responsible for drawing the start button on the board setup screen
;; Type: nil -> Image
(defun draw-button-start (scene)
  (let* ((border (rectangle (+ *start-button-w* 1)
                            (+ *start-button-h* 1)
                            'outline 
                            'black))
         (box (rectangle *start-button-w* *start-button-h* 'solid 'gray))
         (label (text "  Start >" *txt-size* 'white))
         (rect (overlay border box))
         (button (overlay rect label)))
    (place-image button
                 *start-button-x*
                 *start-button-y*
                 scene)))

;; Function responsible for drawing the pause button on the board setup screne
;; Type: nil -> Image
(defun draw-button-pause (scene)
  (let* ((border (rectangle (+ *pause-button-w* 1)
                            (+ *pause-button-h* 1)
                            'outline 
                            'black))
         (box (rectangle *pause-button-w* *pause-button-h* 'solid 'gray))
         (label (text "  Pause " *txt-size* 'white))
         (rect (overlay border box))
         (button (overlay rect label)))
    (place-image button
                 *pause-button-x*
                 *pause-button-y*
                 scene)))

;; Function responsible for drawing the reset button on the board setup screne
;; Type: nil -> Image
(defun draw-button-reset (scene)
  (let* ((border (rectangle (+ *reset-button-w* 1)
                            (+ *reset-button-h* 1)
                            'outline 
                            'black))
         (box (rectangle *reset-button-w* *reset-button-h* 'solid 'gray))
         (label (text "  Reset " *txt-size* 'white))
         (rect (overlay border box))
         (button (overlay rect label)))
    (place-image button
                 *reset-button-x*
                 *reset-button-y*
                 scene)))

; Draws the reset button on the population vs. time graph
(defun draw-button-reset2 (scene)
  (let* ((border (rectangle (+ *reset-button-w* 1)
                            (+ *reset-button-h* 1)
                            'outline 
                            'black))
         (box (rectangle *reset-button-w* *reset-button-h* 'solid 'gray))
         (label (text "  Reset " *txt-size* 'white))
         (rect (overlay border box))
         (button (overlay rect label)))
    (place-image button
                 *reset-button-x2*
                 *reset-button-y2*
                 scene)))


;; Draws the initial menu where the topology is chosen.
;; Type: Struct -> Image
;; Draws the initial menu where the topology is chosen.
;; Type: Struct -> Image
(defun draw-initial-menu (w)
  (let* ((cylinder (place-image (circle 5 'outline 'gray)
                                *cylinder-radio-x*
                                *cylinder-radio-y*
                                (place-image (text "Cylinder" 
                                                   *txt-size*
                                                   *txt-color*)
                                             *cylinder-label-x*
                                             *cylinder-label-y*
                                             (draw-button))))
         (add-moebius (place-image (circle 5 'outline 'gray)
                                   *moebius-radio-x*
                                   *moebius-radio-y*
                                   (place-image (text "Moebius Strip" 
                                                      *txt-size*
                                                      *txt-color*)
                                                *moebius-label-x*
                                                *moebius-label-y*
                                                cylinder)))
         (add-torus (place-image (circle 5 'outline 'gray)
                                 *torus-radio-x*
                                 *torus-radio-y*
                                 (place-image (text "Torus" 
                                                    *txt-size*
                                                    *txt-color*)
                                              *torus-label-x*
                                              *torus-label-y*
                                              add-moebius)))
         (add-klein (place-image (circle 5 'outline 'gray)
                                 *klein-radio-x*
                                 *klein-radio-y*
                                 (place-image (text "Klein Bottle" 
                                                    *txt-size*
                                                    *txt-color*)
                                              *klein-label-x*
                                              *klein-label-y*
                                              add-torus)))
         (add-honeycomb (place-image (circle 5 'outline 'gray)
                                 *honeycomb-radio-x*
                                 *honeycomb-radio-y*
                                 (place-image (text "Honeycomb" 
                                                    *txt-size*
                                                    *txt-color*)
                                              *honeycomb-label-x*
                                              *honeycomb-label-y*
                                              add-klein)))         
         (add-border (place-image (rectangle (- *w-disp* 50)
                                             60
                                             'outline
                                             'gray)
                                  30
                                  (- *title-y* 20)
                                  add-honeycomb))
         (add-border2 (place-image (rectangle (- *w-disp* 50)
                                              (+ (- *klein-label-y* 
                                                    *cylinder-label-y*)
                                                 110)
                                              'outline
                                              'gray)
                                   30
                                   (- *cylinder-label-y* 20)
                                   add-border))
         (add-title (place-image (text "Game of Life" 20 'black)
                                 (- *radio-x* 35)
                                 *title-y*
                                 add-border2))
         (add-title2 (place-image (text "Conway's" 12 'black)
                                  (+ *radio-x* 5)
                                  (- *title-y* 15)
                                  add-title)))
    (cond ((eq (the-world-selected w) 'Cylinder)
           (place-image (circle 2 'solid 'black)
                        *cylinder-radio-x*
                        *cylinder-radio-y*
                        add-title2))
          ((eq (the-world-selected w) 'Moebius)
          (place-image (circle 2 'solid 'black)
                       *moebius-radio-x*
                       *moebius-radio-y*
                       add-title2)) 
           ((eq (the-world-selected w) 'Torus)
           (place-image (circle 2 'solid 'black)
                        *torus-radio-x*
                        *torus-radio-y*
                        add-title2))     
           ((eq (the-world-selected w) 'Klein)
           (place-image (circle 2 'solid 'black)
                        *klein-radio-x*
                        *klein-radio-y*
                        add-title2))
           ((eq (the-world-selected w) 'Honeycomb)
           (place-image (circle 2 'solid 'black)
                        *honeycomb-radio-x*
                        *honeycomb-radio-y*
                        add-title2))            
           (t add-title2))))

;(defun draw-initial-menu (w)
;  (let* ((cylinder (place-image (circle 5 'outline 'gray)
;                                *cylinder-radio-x*
;                                *cylinder-radio-y*
;                                (place-image (text "Cylinder" 
;                                                   *txt-size*
;                                                   *txt-color*)
;                                             *cylinder-label-x*
;                                             *cylinder-label-y*
;                                             (draw-button))))
;         (cylinder-ascii-one (place-image(text " -  .--------."
;                                           *txt-size*
;                                           *txt-color*)
;                                     (+ *cylinder-label-x* 47)
;                                     *cylinder-label-y*
;                                     cylinder))
;         (cylinder-ascii-two (place-image(text "   (             )"
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *cylinder-label-x* 47)
;                                         (+ *cylinder-label-y* 12)
;                                         cylinder-ascii-one))
;         (cylinder-ascii-three (place-image(text "   |~------~|"
;                                                 *txt-size*
;                                                 *txt-color*)
;                                           (+ *cylinder-label-x* 47)
;                                           (+ *cylinder-label-y* 24)
;                                           cylinder-ascii-two))
;         (cylinder-ascii-four (place-image(text "   |              |"
;                                                *txt-size*
;                                                *txt-color*)
;                                          (+ *cylinder-label-x* 47)
;                                          (+ *cylinder-label-y* 36)
;                                          cylinder-ascii-three))
;         (cylinder-ascii-five (place-image(text "   |              |"
;                                                *txt-size*
;                                                *txt-color*)
;                                          (+ *cylinder-label-x* 47)
;                                          (+ *cylinder-label-y* 48)
;                                          cylinder-ascii-four))
;         (cylinder-ascii-six (place-image(text "   \"-..__..-\""
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *cylinder-label-x* 47)
;                                         (+ *cylinder-label-y* 60)
;                                         cylinder-ascii-five))
;         (add-moebius (place-image (circle 5 'outline 'gray)
;                                   *moebius-radio-x*
;                                   *moebius-radio-y*
;                                   (place-image (text "Moebius Strip" 
;                                                      *txt-size*
;                                                      *txt-color*)
;                                                *moebius-label-x*
;                                                *moebius-label-y*
;                                                cylinder-ascii-six)))
;         (moebius-ascii-one (place-image (text " -     ____________"
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *moebius-label-x* 82)
;                                         *moebius-label-y*
;                                         add-moebius))
;         (moebius-ascii-two (place-image (text "    / ___________  \\"
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *moebius-label-x* 82)
;                                         (+ *moebius-label-y* 12)
;                                         moebius-ascii-one))
;         (moebius-ascii-three (place-image (text "    | /                         \\  | "
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *moebius-label-x* 82)
;                                         (+ *moebius-label-y* 24)
;                                         moebius-ascii-two))
;         (moebius-ascii-four (place-image (text "    | \\___________/\\| "
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *moebius-label-x* 82)
;                                         (+ *moebius-label-y* 36)
;                                         moebius-ascii-three))
;         (moebius-ascii-five (place-image (text "    \\_____________/"
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *moebius-label-x* 82)
;                                         (+ *moebius-label-y* 48)
;                                         moebius-ascii-four))
;         (add-torus (place-image (circle 5 'outline 'gray)
;                                 *torus-radio-x*
;                                 *torus-radio-y*
;                                 (place-image (text "Torus" 
;                                                    *txt-size*
;                                                    *txt-color*)
;                                              *torus-label-x*
;                                              *torus-label-y*
;                                              moebius-ascii-five)))
;         (torus-ascii-one (place-image (text " -            _"
;                                             *txt-size*
;                                             *txt-color*)
;                                       (+ *torus-label-x* 42)
;                                       *torus-label-y*
;                                       add-torus))
;         (torus-ascii-two (place-image (text "     ..--\"\"\"_\"\"\"--.."
;                                             *txt-size*
;                                             *txt-color*)
;                                       (+ *torus-label-x* 42)
;                                       (+ *torus-label-y* 12)
;                                       torus-ascii-one))
;         (torus-ascii-three (place-image (text "   (\'        (_)         \')"
;                                               *txt-size*
;                                               *txt-color*)
;                                         (+ *torus-label-x* 42)
;                                         (+ *torus-label-y* 24)
;                                         torus-ascii-two))
;         (torus-ascii-four (place-image (text "    \'\"\"\"--.._..--\"\"\"\'"
;                                              *txt-size*
;                                              *txt-color*)
;                                        (+ *torus-label-x* 42)
;                                        (+ *torus-label-y* 36)
;                                        torus-ascii-three))
;         (add-klein (place-image (circle 5 'outline 'gray)
;                                 *klein-radio-x*
;                                 *klein-radio-y*
;                                 (place-image (text "Klein Bottle" 
;                                                    *txt-size*
;                                                    *txt-color*)
;                                              *klein-label-x*
;                                              *klein-label-y*
;                                              torus-ascii-four)))
;         (add-honeycomb (place-image (circle 5 'outline 'gray)
;                                 *honeycomb-radio-x*
;                                 *honeycomb-radio-y*
;                                 (place-image (text "Honeycomb" 
;                                                    *txt-size*
;                                                    *txt-color*)
;                                              *honeycomb-label-x*
;                                              *honeycomb-label-y*
;                                              add-klein)))         
;         (add-border (place-image (rectangle (- *w-disp* 50)
;                                             60
;                                             'outline
;                                             'gray)
;                                  30
;                                  (- *title-y* 20)
;                                  add-honeycomb))
;         (add-border2 (place-image (rectangle (- *w-disp* 50)
;                                              (+ (- *klein-label-y* 
;                                                    *cylinder-label-y*)
;                                                 110)
;                                              'outline
;                                              'gray)
;                                   30
;                                   (- *cylinder-label-y* 20)
;                                   add-border))
;         (add-title (place-image (text "Game of Life" 20 'black)
;                                 (- *radio-x* 35)
;                                 *title-y*
;                                 add-border2))
;         (add-title2 (place-image (text "Conway's" 12 'black)
;                                  (+ *radio-x* 5)
;                                  (- *title-y* 15)
;                                  add-title)))
;    (cond ((eq (the-world-selected w) 'Cylinder)
;           (place-image (circle 2 'solid 'black)
;                        *cylinder-radio-x*
;                        *cylinder-radio-y*
;                        add-title2))
;          ((eq (the-world-selected w) 'Moebius)
;          (place-image (circle 2 'solid 'black)
;                       *moebius-radio-x*
;                       *moebius-radio-y*
;                       add-title2)) 
;           ((eq (the-world-selected w) 'Torus)
;           (place-image (circle 2 'solid 'black)
;                        *torus-radio-x*
;                        *torus-radio-y*
;                        add-title2))     
;           ((eq (the-world-selected w) 'Klein)
;           (place-image (circle 2 'solid 'black)
;                        *klein-radio-x*
;                        *klein-radio-y*
;                        add-title2))
;           ((eq (the-world-selected w) 'Honeycomb)
;           (place-image (circle 2 'solid 'black)
;                        *honeycomb-radio-x*
;                        *honeycomb-radio-y*
;                        add-title2))            
;           (t add-title2))))

;; Draws the columns on the grid where the sim is setup and run by drawing
;; lines down the entire height of the board.
;; Type: nat Image -> Image
(defun draw-columns (current-x dimensions scene)
  (if (zp current-x)
      scene
      (draw-columns (- current-x 1)
      		    dimensions
                    (add-line scene 
                              (* current-x (/ *w-disp* dimensions))
                              0
                              (* current-x (/ *w-disp* dimensions))
                              *grid-height*
                              'black))))

;; Draws the rows on the grid where the sim is setup and run by drawing
;; lines across the entire width of the board.
;; Type: nat Image -> Image
(defun draw-rows (current-y dimensions scene)
  (if (zp current-y)
      scene
      (draw-rows (- current-y 1)
      		 dimensions
                 (add-line scene
                           0
                           (* current-y (/ *grid-height* dimensions))
                           *w-disp*
                           (* current-y (/ *grid-height* dimensions))
                           'black))))

;; Draws the grid by calling draw-rows and draw-columns to draw lines across
;; the board.
;; Type: nil -> Image
(defun draw-grid (dimensions scene)
  (draw-rows dimensions
  	     dimensions
             (draw-columns dimensions
             		   dimensions
                           scene)))

;;draw individual comb
(defconst *comb-side-length* 15)
(defconst *comb-angle-up-length* 9)
(defconst *comb-angle-over-length* 12)

(set-ignore-ok t)
(defun draw-honeycomb (current-x current-y scene)
  (let* ((x0 current-x)
         (y0 (+ *comb-side-length* current-y))
         (left-line (add-line scene 
                              current-x 
                              current-y
                              x0
                              y0
                              'black))
         (x1 current-x)
         (y1 current-y)
         (x2 (+ *comb-angle-over-length* current-x))
         (y2 (- current-y *comb-angle-up-length*))
         (top-left-line (add-line left-line 
                                  x1 
                                  y1 
                                  x2
                                  y2 'black))
         (x3 (+ *comb-angle-over-length* 
                                      (+ *comb-angle-over-length* current-x)))
         (y3 (+ (- current-y *comb-angle-up-length*) 
                                      *comb-angle-up-length*))
         (top-right-line (add-line top-left-line 
                                   x2
                                   y2
                                   x3
                                   y3
                                   'black))
         (x4 x3)
         (y4 (+ y3 *comb-side-length*))
         (right-line (add-line top-right-line 
                               x3
                               y3
                               x4
                               y4
                               'black))
         (x5 (- x4 *comb-angle-over-length*))
         (y5 (+ y4 *comb-angle-up-length*))
         (bottom-right-line (add-line right-line
                                      x4
                                      y4
                                      x5
                                      y5
                                      'black))
         (bottom-left-line (add-line bottom-right-line
                                     x5
                                     y5
                                     x0
                                     y0
                                     'black)))
  bottom-left-line))

(defun draw-honeycombs-col (col current-x current-y scene)
  (cond ((zp col)
        scene)
        ((> col 0)
         (let* ((next-x (+ current-x (* *comb-angle-over-length* 2)))
                (next-y current-y))
           (draw-honeycombs-col (- col 1) 
                            next-x
                            next-y 
                            (draw-honeycomb current-x current-y scene))))))

(defun draw-honeycombs-row (row col-total orig-x current-y scene)
  (cond ((zp row)
         scene)
        ((> row 0)
         (let* ((next-x 
                 (if (= (mod row 2) 1)
                     (- orig-x *comb-angle-over-length*)
                     orig-x))
                (next-y (if (= row col-total)
                            current-y
                            (+ current-y (+ *comb-side-length* *comb-angle-up-length*)))))
           (draw-honeycombs-row (- row 1)
                            col-total
                            orig-x
                            next-y 
                            (draw-honeycombs-col col-total next-x next-y scene))))))

;;draws honeycomb grid
(defun draw-honeycomb-grid (dimensions scene)
  (draw-honeycombs-row dimensions dimensions 8 8 scene))

;(defconst *honeycomb* (draw-honeycomb-grid 16 (empty-scene *w-disp* *h-disp*)))

; Draws the grid size selector radio buttons and labels
; int Image -> Image
(defun draw-size-selector (size scene)
  (let* ((size-twenty (place-image (circle 5 'outline 'gray)
                                   *size-radio-x-20*
                                   *size-radio-y-20*
                                   (place-image (text "20 x 20" 
                                                      *txt-size*
                                                      *txt-color*)
                                                *size-label-x-20*
                                                *size-label-y-20*
                                                scene)))
         (size-fifty (place-image (circle 5 'outline 'gray)
                                   *size-radio-x-50*
                                   *size-radio-y-50*
                                   (place-image (text "50 x 50" 
                                                      *txt-size*
                                                      *txt-color*)
                                                *size-label-x-50*
                                                *size-label-y-50*
                                                size-twenty)))
         (size-hundred (place-image (circle 5 'outline 'gray)
                                   *size-radio-x-100*
                                   *size-radio-y-100*
                                   (place-image (text "100x100" 
                                                      *txt-size*
                                                      *txt-color*)
                                                *size-label-x-100*
                                                *size-label-y-100*
                                                size-fifty))))
    (cond ((= size 50)
           (place-image (circle 2 'solid 'black)
                        *size-radio-x-50*
                        *size-radio-y-50*
                        size-hundred))
          ((= size 100)
           (place-image (circle 2 'solid 'black)
                        *size-radio-x-100*
                        *size-radio-y-100*
                        size-hundred))           
          (t 
           (place-image (circle 2 'solid 'black)
                        *size-radio-x-20*
                        *size-radio-y-20*
                        size-hundred)))))

;; Draws blue rectangles in the cells that the user has clicked to select
;; when setting up the sim.
;; Type: list Image -> Image
(defun draw-selected-cells (cells dimensions scene)
  (if (consp cells)
      (let* ((x-offset (* (- (car cells) 1) (floor *w-disp* dimensions)))
            (row-number (floor (- (car cells) 1) dimensions))
            (new-scene
             (place-image (rectangle (floor *w-disp* dimensions) 
             			     (floor *grid-height* dimensions) 
             			     'solid 
             			     'blue)
                          (mod x-offset *w-disp*)
                          (* row-number (floor *grid-height* dimensions))
                          scene)))
        (draw-selected-cells (cdr cells) dimensions new-scene))
      scene))

; the honeycomb rows don't line up like the square grid, they are
; staggered, so we have to adjust in alternating rows.
; Type: int int -> int
(defun adjust-x-in-odd-row (x width)
  (if (< (mod x width)
         (* *comb-angle-over-length* 2))
      *comb-angle-over-length*
      0))

; Draws blue rectangles in the cells the user has clicked on (revived) in the
; honeycomb grid.
; Type: list int Image -> Image
(defun draw-selected-cells-honeycomb (cells dimensions scene)
  (if (consp cells)
      (let* ((grid-width (* (* *comb-angle-over-length* 2)
                            dimensions))
             (grid-height (* (+ *comb-side-length* 
                                (* *comb-angle-up-length* 2)) 
                             dimensions))
             (x-offset (* (- (car cells) 1) (floor grid-width dimensions)))
             (row-number (floor (- (car cells) 1) dimensions)))
        (if (>= row-number 1)
            (if (oddp row-number)
                (let* ((adjustment (adjust-x-in-odd-row x-offset grid-width))
                      (new-scene
                       (place-image (rectangle (* *comb-angle-over-length* 2) 
                                               *comb-side-length* 
                                               'solid 
                                               'blue)
                                    (- (mod x-offset grid-width) 3)
                                    ;(- (+ (mod x-offset grid-width) 
                                    ;   (* *comb-angle-over-length* 2)) 
                                    ;   *comb-angle-over-length*)
                                    (- (+ (* row-number 
                                             (floor grid-height dimensions)) 
                                          8) 
                                       (* row-number *comb-angle-up-length*))
                                    scene)))
              (draw-selected-cells-honeycomb (cdr cells) dimensions new-scene))
                (let ((new-scene
                       (place-image (rectangle (* *comb-angle-over-length* 2) 
                                               *comb-side-length* 
                                               'solid 
                                               'blue)
                                    (+ (mod x-offset grid-width) 
                                       8);(* *comb-angle-over-length* 2))
                                    (- (+ (* row-number 
                                             (floor grid-height dimensions)) 
                                          8) 
                                       (* row-number *comb-angle-up-length*))
                                    scene)))
              (draw-selected-cells-honeycomb (cdr cells) dimensions new-scene)))                
            (let ((new-scene
             (place-image (rectangle (* *comb-angle-over-length* 2) 
             			     *comb-side-length* 
             			     'solid 
             			     'blue)
                          ;(+ (mod x-offset grid-width) 
                          ;   (* *comb-angle-over-length* 2))
                          (+ x-offset 8)
                          (+ (* row-number (floor grid-height dimensions)) 8)
                          scene)))
        (draw-selected-cells-honeycomb (cdr cells) dimensions new-scene))))
      scene))

;;convert a list of rational numbers into a string
(defun rat-list->string (rat-list)
  (if (endp rat-list)
      ""
      (concatenate 'string 
                   (rat->str (car rat-list) 0) 
                   " " 
                   (rat-list->string (cdr rat-list)))))

;; Draws list of selected cells
;; Type: list Image -> Image
(defun draw-selected-cells-list (cells scene)
  (place-image (text (rat-list->string cells) 
                     *txt-size* 
                     *txt-color*) 
               20 
               400 
               scene))

;; Draw a label that specifies the selected topology.
(defun draw-topo-label (topo scene)
  (case topo
    ('Cylinder (place-image (text "Cylinder"      *txt-size* *txt-color*) 
                            *topo-label-x* 
                            *topo-label-y* 
                            scene))
    ('Moebius  (place-image (text "Moebius Strip" *txt-size* *txt-color*) 
                            (- *topo-label-x* 40) 
                            *topo-label-y* 
                            scene))
    ('Torus    (place-image (text "Torus"         *txt-size* *txt-color*) 
                            (+ *topo-label-x* 10) 
                            *topo-label-y* 
                            scene))
    ('Klein    (place-image (text "Klein Bottle"  *txt-size* *txt-color*) 
                            (- *topo-label-x* 30) 
                            *topo-label-y* 
                            scene))
    ('Honeycomb    (place-image (text "Honeycomb"  *txt-size* *txt-color*) 
                            (- *topo-label-x* 30) 
                            *topo-label-y* 
                            scene))))    

; Draws the "Graph" button that lets the user graph population vs. time
; Type: Image -> Image
(defun draw-button-graph (scene)
  (let* ((border (rectangle (+ *graph-button-w* 1)
                            (+ *graph-button-h* 1)
                            'outline 
                            'black))
         (box (rectangle *graph-button-w* *graph-button-h* 'solid 'gray))
         (label (text "  Graph  " *txt-size* 'white))
         (rect (overlay border box))
         (button (overlay rect label)))
    (place-image button
                 *graph-button-x*
                 *graph-button-y*
                 scene)))

;; Draws blue rectangles in the cells that the user has clicked to select
;; when setting up the sim.
;; Type: Structure -> Image
(defun draw-board-setup (w)
  (draw-topo-label (the-world-selected w) 
                   (draw-selected-cells-list (alive-cells-list 
                                              (the-world-board w))
                                        (draw-grid (the-world-size w)
                                        (draw-selected-cells 
                                           (alive-cells-list (the-world-board w))
                                           (the-world-size w)
                                           (draw-button-start 
                                            (draw-size-selector (the-world-size w)
                                            (empty-scene *w-disp* *h-disp*))))))))

;; Draws the honeycomb grid and selected cells during the setup phase
;; Type: struct -> Image
(defun draw-honeycomb-board-setup (w)
  (draw-topo-label (the-world-selected w) 
                   (draw-selected-cells-list (alive-cells-list 
                                              (the-world-board w))
                                        ;(draw-honeycomb-grid (the-world-size w)
                                        (draw-selected-cells-honeycomb 
                                           (alive-cells-list (the-world-board w))
                                           (the-world-size w)
                                           (draw-button-start 
                                            (draw-honeycomb-grid 16 (empty-scene *w-disp* *h-disp*)))))))
                                            ;(empty-scene *w-disp* *h-disp*)))))))

;; Draws the grid and alive cells and size selector as the game is running.
;; Type: struct -> Image
(defun draw-sim (w)
  (let ((board (draw-topo-label (the-world-selected w)
                                (draw-grid (the-world-size w)
                                (draw-selected-cells 
                                 (alive-cells-list (the-world-board w))
                                 (the-world-size w)
                                 (draw-button-reset 
                                  (draw-button-pause 
                                   (draw-size-selector (the-world-size w)
                                         (empty-scene *w-disp* *h-disp*)))))))))
    (if (and (or (endp (the-world-board w))
                 (>= (the-world-timestamp w) *stats-limit*))
             (consp (the-world-population-sizes w)))
        (draw-button-graph board)
        board)))    

;; Draws the honeycomb grid and alive cells as the game is running.
;; Type: struct -> Image
(defun draw-honeycomb-sim (w)
  (let ((board (draw-topo-label (the-world-selected w)
                                ;(draw-honeycomb-grid (the-world-size w)
                                (draw-selected-cells-honeycomb 
                                 (alive-cells-list (the-world-board w))
                                 (the-world-size w)
                                 (draw-button-reset 
                                  (draw-button-pause 
                                   (draw-honeycomb-grid 16 (empty-scene *w-disp* *h-disp*))))))))
                                   ;(empty-scene *w-disp* *h-disp*))))))))
    (if (and (or (endp (the-world-board w))
                 (>= (the-world-timestamp w) *stats-limit*))
             (consp (the-world-population-sizes w)))
        (draw-button-graph board)
        board)))

;; Draws the x-axis on the population vs. time graph
;; Type: Image str -> Image
(defun draw-x-axis (scene label)
  (place-image label
               *x-axis-label-x*
               *x-axis-label-y*
               (add-line scene
                         *x-axis-x1*
                         *x-axis-y*
                         *x-axis-x2*
                         *x-axis-y*
                         'black)))

;; Draws the y-axis on the population vs. time graph
;; Type: Image -> Image
(defun draw-y-axis (scene)
  (add-line scene
            *y-axis-x*
            *y-axis-y1*
            *y-axis-x*
            *y-axis-y2*
            'black))

;; Draws num tick marks on scene, which should be a drawing with the y-axis
;; of the graph on it.
;; Type: nat nat Image -> Image
(defun draw-y-ticks (num max scene)
  (if (zp num)
      scene
      (let ((label (* (+ (- *y-tick-marks* num) 1)
                      (/ max (+ *y-tick-marks* 1)))))
        (draw-y-ticks (- num 1)
                      max
                      (place-image (text (rat->str label 2)
                                         8
                                         'black)
                                   (- *y-axis-x* 25)
                                   (+ (* *y-tick-width* num)
                                      *y-axis-y2*)
                                   (add-line scene
                                             (+ *y-axis-x* 5)
                                             (+ (* *y-tick-width* num)
                                                *y-axis-y2*)
                                             (- *y-axis-x* 5)
                                             (+ (* *y-tick-width* num)
                                                *y-axis-y2*)
                                             'black))))))

;; Draws num tick marks on scene, which should be a drawing with the x-axis
;; of the graph on it.
;; Type: nat nat Image -> Image
(defun draw-x-ticks (num max scene)
  (if (zp num)
      scene
      (let ((label (* (+ (- *x-tick-marks* num) 1)
                      (/ max (+ *x-tick-marks* 1)))))
      (draw-x-ticks (- num 1)
                    max
                  (place-image (text (rat->str label 2)
                                     8
                                     'black)
                               (- *x-axis-x2*
                                  (* *x-tick-width* num))
                               (+ *x-axis-y* 10)
                               (add-line scene
                                         (- *x-axis-x2*
                                            (* *x-tick-width* num))
                                         (+ *x-axis-y* 5)
                                         (- *x-axis-x2*
                                            (* *x-tick-width* num))
                                         (- *x-axis-y* 5)
                                         'black))))))

;; Plots all of the (time, population) coordinate pairs in populations on the
;; population vs. time graph on scene.
;; Type: list nat nat Image -> Image
(defun plot-populations (populations xmax ymax scene)
  (if (consp populations)
      (let* ((x-interval (floor xmax (+ *x-tick-marks* 1)))
             (x (+ *x-axis-x1*
                   (* *x-tick-width* (/ (caar populations) x-interval))))
             (y-interval (floor ymax (+ *y-tick-marks* 1)))
             (y (- *y-axis-y1*
                   (* *y-tick-width* (/ (cdr (car populations)) y-interval))))
            (newscene (place-image (circle 2 'solid 'blue)
                                   (floor x 1)
                                   (floor y 1)
                                   scene)))
        (plot-populations (cdr populations)
                        xmax
                        ymax
                        newscene))
      scene))

;; Draws a horizontal line that crosses the y-axis at the mean population
;; denoting the mean population.
;; Type: nat nat Image -> Image
(defun plot-mean (mean ymax scene)
  (let* ((y-interval (floor ymax (+ *y-tick-marks* 1)))
         (y (- *y-axis-y1*
               (* *y-tick-width* (/ mean y-interval)))))
    (add-line scene
              (- *x-axis-x1* 10)
              y
              (+ *x-axis-x2* 10)
              y
              'gray)))

;; Calculates the mean of the integer list numbers recursively.
;; Type: list integer nat -> rational
;(defun calc-mean (numbers sum length)
;  (if (consp numbers)
;      (calc-mean (cdr numbers)
;                 (+ sum (car numbers))
;                 length)
;      (/ sum length)))

(defun sum-list (numbers sum)
  (if (and (consp numbers)
           (integerp sum)
           (integerp (car numbers)))
      (sum-list (cdr numbers) (+ sum (car numbers)))
      sum))

;; Calculates the mean of the integer list numbers.
;; Type: list -> rational
(defun calculate-mean (numbers)
  (if (not (integer-listp numbers))
      0
      (/ (sum-list numbers 0)
         (length numbers))))
      ;(calc-mean numbers
      ;           0
      ;           (length numbers))))

;; Draws the graph of population vs. time.
;; Type: struct -> Image
(defun graph-populations (w)
  (let* ((mean (calculate-mean (the-world-population-sizes w)))
         (xmax (caar (last (the-world-population-and-time w))))
         (ymax (car (last (the-world-population-sizes w))))
         (xmax2 (+ xmax
                   (- (+ *x-tick-marks* 1)
                      (mod xmax (+ *x-tick-marks* 1)))))
         (ymax2 (+ ymax
                   (- (+ *y-tick-marks* 1) 
                      (mod ymax (+ *y-tick-marks* 1)))))
         (x-axis (draw-x-ticks *x-tick-marks*
                               xmax2
                               (draw-x-axis (draw-button-reset2 
                                             (empty-scene *w-disp* *h-disp*))
                                            (text "Time (timesteps)" 10 'black))))
         (y-axis (draw-y-ticks *y-tick-marks*
                               ymax2
                               (draw-y-axis x-axis)))
         (graph (place-image (text "Population Size vs Time" 20 'black)
                 *graph-title-x*
                 *graph-title-y*
                 y-axis))
         (plot (plot-mean mean
                          ymax2
                          graph)))
    (plot-populations (the-world-population-and-time w)
                    xmax2
                    ymax2
                    plot)))         
         

;; Draws the interface based on the current state of the world.
;; Type: Structure -> Image
(defun world-image (w)
  (cond ((= (the-world-phase w) *initial-menu*) (draw-initial-menu w))
        ((= (the-world-phase w) *board-setup*) 
         (if (eq (the-world-selected w) 'Honeycomb)
             (draw-honeycomb-board-setup w)
             (draw-board-setup w)))
        ((= (the-world-phase w) *run-sim*) 
         (if (eq (the-world-selected w) 'Honeycomb)
             (draw-honeycomb-sim w)
             (draw-sim w)))
        ((= (the-world-phase w) *graph*) (graph-populations w))
        (t nil)))

;; Transforms the world by updating the board based on the current configuration
;; of alive and dead cells.
;; Type: struct -> struct
(defun world-next (w)
  (cond ((= (the-world-phase w) *run-sim*)
         (let ((board (update-tree (the-world-board w) 
                                   (the-world-selected w)
                                   (the-world-size w))))
                 (if (and (< (length (the-world-population-sizes w)) 
                             *stats-limit*)
                          (consp (the-world-board w)))
                     (the-world (the-world-selected w)
                                *run-sim*
                                board
                                (append (list (length (keys (the-world-board w))))
                                        (the-world-population-sizes w))
                                (cons (cons (the-world-timestamp w)
                                            (length (keys (the-world-board w))))
                                        (the-world-population-and-time w))
                                (+ (the-world-timestamp w) 1)
                                (the-world-size w)
                                (the-world-cursor-location w))
                     (the-world (the-world-selected w)
                                *run-sim*
                                board
                                (the-world-population-sizes w)
                                (the-world-population-and-time w)
                                (+ (the-world-timestamp w) 1)
                                (the-world-size w)
                                (the-world-cursor-location w)))))                     
        (t w)))

;; Changes the menu selection to the topology that the user clicked on.
;; Type: Structure int int -> Structure
(defun change-menu-selection (w x y)
  (cond ((< (+ (* (- x *cylinder-radio-x*)
                  (- x *cylinder-radio-x*))
               (* (- y *cylinder-radio-y*)
                  (- y *cylinder-radio-y*)))
            100)
         (the-world 'Cylinder
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    20
                    (the-world-cursor-location w)))
        ((< (+ (* (- x *moebius-radio-x*)
                  (- x *moebius-radio-x*))
               (* (- y *moebius-radio-y*)
                  (- y *moebius-radio-y*)))
            100)
         (the-world 'Moebius
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    20
                    (the-world-cursor-location w)))
        ((< (+ (* (- x *torus-radio-x*)
                  (- x *torus-radio-x*))
               (* (- y *torus-radio-y*)
                  (- y *torus-radio-y*)))
            100)
         (the-world 'Torus
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    20
                    (the-world-cursor-location w)))
        ((< (+ (* (- x *klein-radio-x*)
                  (- x *klein-radio-x*))
               (* (- y *klein-radio-y*)
                  (- y *klein-radio-y*)))
            100)
         (the-world 'Klein
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    20
                    (the-world-cursor-location w)))
        ((< (+ (* (- x *honeycomb-radio-x*)
                  (- x *honeycomb-radio-x*))
               (* (- y *honeycomb-radio-y*)
                  (- y *honeycomb-radio-y*)))
            100)
         (the-world 'Honeycomb
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    16
                    (the-world-cursor-location w)))        
        ((and (>= x *next-button-x*)
              (<= x (+ *next-button-x* *next-button-w*))
              (>= y *next-button-y*)
              (<= y (+ *next-button-y* *next-button-h*)))
         (the-world (the-world-selected w)
                    *board-setup*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    (the-world-size w)
                    (the-world-cursor-location w)))
        (t w)))

;; Changes the selected grid size when the user clicks on one of the size
;; radio buttons.
;; Type: struct int int -> struct
(defun change-size-selection (w x y)
  (cond ((< (+ (* (- x *size-radio-x-20*)
                  (- x *size-radio-x-20*))
               (* (- y *size-radio-y-20*)
                  (- y *size-radio-y-20*)))
            100)
         (the-world (the-world-selected w)
                    (the-world-phase w)
                    (the-world-board w)
                    (the-world-population-sizes w)
                    (the-world-population-and-time w)
                    (the-world-timestamp w)
                    20
                    (the-world-cursor-location w)))
        ((< (+ (* (- x *size-radio-x-50*)
                  (- x *size-radio-x-50*))
               (* (- y *size-radio-y-50*)
                  (- y *size-radio-y-50*)))
            100)
         (the-world (the-world-selected w)
                    (the-world-phase w)
                    (the-world-board w)
                    (the-world-population-sizes w)
                    (the-world-population-and-time w)
                    (the-world-timestamp w)
                    50
                    (the-world-cursor-location w)))
        ((< (+ (* (- x *size-radio-x-100*)
                  (- x *size-radio-x-100*))
               (* (- y *size-radio-y-100*)
                  (- y *size-radio-y-100*)))
            100)
         (the-world (the-world-selected w)
                    (the-world-phase w)
                    (the-world-board w)
                    (the-world-population-sizes w)
                    (the-world-population-and-time w)
                    (the-world-timestamp w)
                    100
                    (the-world-cursor-location w)))
        (t w)))


;; The x coordinate registered by the event handler is off slightly, it
;; usually registers the tip of the pointer as being slightly ahead of
;; its actual location, so this method adjusts the registered coordinate.
;; This is only a problem when trying to decide what cell the user clicked
;; on in the board setup phase.
;; Type: int -> int
(defun adjust-x (x dimensions)
  (if (< (mod x (floor *w-disp* dimensions)) 
         (/ (floor *w-disp* dimensions) 
            (floor *grid-height* (* dimensions 2))))
      (- x (/ (floor *w-disp* dimensions) 
              (floor *grid-height* (* dimensions 2))))
      x))

;; The x coordinate registered by the event handler is off slightly, it
;; usually registers the tip of the pointer as being slightly ahead of
;; its actual location, so this method adjusts the registered coordinate.
;; This is only a problem when trying to decide what cell the user clicked
;; on in the board setup phase.
;; Type: int -> int
(defun adjust-y (y dimensions)
  (if (< (mod y (floor *grid-height* dimensions)) 
         (/ (floor *grid-height* dimensions) 
            (floor *grid-height* (* dimensions 2))))
      (- y (/ (floor *grid-height* dimensions) 
              (floor *grid-height* (* dimensions 2))))
      y))

;; Changes the board setup by finding the cell that the user clicked on
;; and adding it to the list of selected cells.
;; Type: Structure int int -> Structure
(defun board-setup-change (w x y)
  (let* ((adjusted-x (adjust-x x (the-world-size w)))
        (adjusted-y (adjust-y y (the-world-size w)))
        (i (floor adjusted-y (/ *grid-height* (the-world-size w))))
        (j (+ (floor adjusted-x (/ *w-disp* (the-world-size w))) 1)))
    (cond ((and (>= x *start-button-x*)
                (<= x (+ *start-button-x* *start-button-w*))
                (>= y *start-button-y*)
                (<= y (+ *start-button-y* *start-button-h*)))
             (the-world (the-world-selected w)
                        *run-sim*
                        (the-world-board w)
                        (the-world-population-sizes w)
                        (the-world-population-and-time w)
                        (the-world-timestamp w)
                        (the-world-size w)
                        (the-world-cursor-location w)))
          ((and (<= i (the-world-size w))
                (<= j (the-world-size w))
                (<= (+ (* i (the-world-size w)) j)
                    (* (the-world-size w) (the-world-size w)))
	        (not (alive? (+ (* i (the-world-size w)) j) (the-world-board w))))
             (the-world (the-world-selected w)
                        *board-setup*
                        (alive-cells-insert (the-world-board w) 
					    (+ (* i (the-world-size w)) j))
                        (the-world-population-sizes w)
                        (the-world-population-and-time w)
                        (the-world-timestamp w)
                        (the-world-size w)
                        (+ (* i (the-world-size w)) j)))
	  ((alive? (+ (* i (the-world-size w)) j) (the-world-board w))
	     (the-world (the-world-selected w)
			*board-setup*
			(alive-cells-kill (the-world-board w) 
					  (+ (* i (the-world-size w)) j))
                        (the-world-population-sizes w)
                        (the-world-population-and-time w)
                        (the-world-timestamp w)
                        (the-world-size w)
                        (+ (* i (the-world-size w)) j)))
          (t (change-size-selection w x y)))))

;; Adjusts the reported x-coordinate because the honeycomb grid is not drawn
;; flush with the edge of the window, so we must adjust for this offset in
;; calculations.
(defun adjust-x-honeycomb (x i)
  (if (oddp i)
      (+ x 20)
      (+ x 13)))
  ;(if (evenp i)
  ;    (- x 8)
  ;    (- x (- 8 *comb-angle-over-length*))))

(defun adjust-cell-id (id x size)
  (if (and (zp (mod id size))
           (< x 50))
      (+ id 1)
      id))

;; Adjusts the reported y coordinate since the honeycomb rows overlap slightly.
;; An adjustment must be made for this fact.
(defun adjust-y-honeycomb (y)
  (if (> y 100)
  (+ (+ (- y 6) *comb-side-length*) (* (ceiling y (+ *comb-side-length*
                        (* *comb-angle-up-length* 2)))
          *comb-angle-up-length*))
  (+ (- y 12) (* (ceiling y (+ *comb-side-length*
                        (* *comb-angle-up-length* 2)))
          *comb-angle-up-length*))))

;; Changes the board setup by finding the cell that the user clicked on
;; and adding it to the list of selected cells or deselecting already selected
;; cells.
;; Type: Structure int int -> Structure
(defun board-setup-change-honeycomb (w x y)
  (let* ((grid-width (* (* *comb-angle-over-length* 2)
                       (the-world-size w)))
         (adjusted-y (adjust-y-honeycomb (- y (- 8 *comb-angle-up-length*))))
        (i (floor (- adjusted-y 0);(- 8 *comb-angle-up-length*))
                  (+ *comb-side-length*
                     (* *comb-angle-up-length* 2))))
        (adjusted-x (adjust-x-honeycomb x i))
        (j (floor adjusted-x (/ grid-width (the-world-size w))))
        (cell-id (+ (* i (the-world-size w)) j))
        (adjusted-cell-id (adjust-cell-id cell-id x (the-world-size w))))
    (cond ((and (>= x *start-button-x*)
                (<= x (+ *start-button-x* *start-button-w*))
                (>= y *start-button-y*)
                (<= y (+ *start-button-y* *start-button-h*)))
             (the-world (the-world-selected w)
                        *run-sim*
                        (the-world-board w)
                        (the-world-population-sizes w)
                        (the-world-population-and-time w)
                        (the-world-timestamp w)
                        (the-world-size w)
                        (the-world-cursor-location w)))
          ((and (<= i (the-world-size w))
                (<= j (the-world-size w))
                (<= adjusted-cell-id
                    (* (the-world-size w) (the-world-size w)))
	        (not (alive? adjusted-cell-id (the-world-board w))))
             (the-world (the-world-selected w)
                        *board-setup*
                        (alive-cells-insert (the-world-board w) 
					    adjusted-cell-id)
                        (the-world-population-sizes w)
                        (the-world-population-and-time w)
                        (the-world-timestamp w)
                        (the-world-size w)
                        (+ (* i (the-world-size w)) j)))
	  ((alive? adjusted-cell-id (the-world-board w))
	     (the-world (the-world-selected w)
			*board-setup*
			(alive-cells-kill (the-world-board w) 
					  adjusted-cell-id)
                        (the-world-population-sizes w)
                        (the-world-population-and-time w)
                        (the-world-timestamp w)
                        (the-world-size w)
                        (+ (* i (the-world-size w)) j)))
          (t w))))

;; monitors mouse changes while the game is running
(defun run-sim-change (w x y)
  (cond ((and (>= x *pause-button-x*)
              (<= x (+ *pause-button-x* *pause-button-w*))
              (>= y *pause-button-y*)
              (<= y (+ *pause-button-y* *pause-button-h*)))
         (the-world (the-world-selected w)
                    *board-setup*
                    (the-world-board w)
                    (the-world-population-sizes w)
                    (the-world-population-and-time w)
                    (the-world-timestamp w)
                    (the-world-size w)
                    (the-world-cursor-location w)))
        ((and (>= x *reset-button-x*)
              (<= x (+ *reset-button-x* *reset-button-w*))
              (>= y *reset-button-y*)
              (<= y (+ *reset-button-y* *reset-button-h*)))
         (the-world (the-world-selected w)
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    20
                   (the-world-cursor-location w)))
        ((and (>= x *graph-button-x*)
              (<= x (+ *graph-button-x* *graph-button-w*))
              (>= y *graph-button-y*)
              (<= y (+ *graph-button-y* *graph-button-h*))
              (= (the-world-phase w) *run-sim*)
              (or (>= (the-world-timestamp w) *stats-limit*)
                  (endp (the-world-board w)))
              (consp (the-world-population-sizes w)))
           (the-world (the-world-selected w)
                      *graph*
                      (the-world-board w)
                      (merge-sort (the-world-population-sizes w))
                      (merge-sort-by-time (the-world-population-and-time w))
                      (the-world-timestamp w)
                      (the-world-size w)
                      (the-world-cursor-location w)))
        (t (if (eq (the-world-selected w) 'Honeycomb)
               w
               (change-size-selection w x y)))))

;; Responds to mouse clicks while the population vs. time graph is displayed.
(defun graph-mouse-clicked (w x y)
  (cond ((and (>= x *reset-button-x2*)
              (<= x (+ *reset-button-x2* *reset-button-w*))
              (>= y *reset-button-y2*)
              (<= y (+ *reset-button-y2* *graph-button-h*)))
         (the-world (the-world-selected w)
                    *initial-menu*
                    (alive-cells-constructor)
                    nil
                    nil
                    1
                    20
                   (the-world-cursor-location w)))
        (t w)))


(set-ignore-ok t)
(set-irrelevant-formals-ok t)
(defun world-change (w k)
  w)

;; Changes the world by responding to mouse clicks in the appropriate manner.
;; Type: Structure int int symbol -> Structure
(defun world-mouse-change (w x y m)
  (cond ((eq m 'button-down) 
         (cond ((= (the-world-phase w) *initial-menu*)
                (change-menu-selection w x y))
               ((= (the-world-phase w) *board-setup*)
                (if (eq (the-world-selected w) 'Honeycomb)
                    (board-setup-change-honeycomb w x y)
                    (board-setup-change w x y)))
               ((= (the-world-phase w) *run-sim*)
                (run-sim-change w x y))
               ((= (the-world-phase w) *graph*)
                (graph-mouse-clicked w x y))
               (t w)))
        (t w)))  
  

; END OF YOUR SOURCE CODE

(big-bang *w-disp* *h-disp* *tick* *new-world*)
(on-redraw world-image)
(on-tick-event world-next)
(on-key-event world-change)
(on-mouse-event world-mouse-change)


;;-----------------------------------------------------------------------------
;;          THEOREMS
;;-----------------------------------------------------------------------------

(defthm alive-cells?-delivers-boolean
  (booleanp (alive-cells? tr)))

(defthm alive-cells-constructor-delivers-tree
  (tree? (alive-cells-constructor)))

(defthm dead-neighbors-insert-delivers-list
  (consp (dead-neighbors-insert x y)))

(defthm dead-neighbors-insert-list-delivers-list
  (implies (and (true-listp x)
                (true-listp y))
           (true-listp (dead-neighbors-insert-list x y))))

(defthm dead-neighbors-list-delivers-true-list
  (true-listp (dead-neighbors-list x)))

(defthm cell-in-range?-delivers-boolean
  (booleanp (cell-in-range? x y)))

(defthm moebius-klein-neighbor-delivers-int
  (implies (and (integerp x)
                (integerp y))
           (integerp (moebius-klein-neighbor x y))))

(defthm get-topo-top-neighbor-delivers-int
  (implies (and (integerp x)
                (integerp z)
                (or (eq y 'Klein)
                    (eq y 'Torus)))
           (integerp (get-topo-top-neighbor x y z))))
  
(defthm get-top-neighbor-delivers-int
  (implies(and (natp x)
               (symbolp y)
               (or (eq y 'Klein)
                   (eq y 'Torus))
               (integerp z)
               (cell-in-range? x z))
          (integerp (get-top-neighbor x y z))))

(defthm get-topo-bottom-neighbor-delivers-int
  (implies (and (natp x)
               (symbolp y)
               (or (eq y 'Klein)
                   (eq y 'Torus))
               (integerp z))
           (integerp (get-topo-bottom-neighbor x y z))))
  
(defthm get-bottom-neighbor-delivers-int
  (implies(and (natp x)
               (integerp z)
               (cell-in-range? x z)
               (symbolp y)
               (or (eq y 'Klein)
                   (eq y 'Torus)))
          (integerp (get-bottom-neighbor x y z))))

(defthm get-topo-left-neighbor-delivers-int
  (implies (and (integerp x)
                (integerp z)
                (or (eq y 'Cylinder)
                    (eq y 'Moebius)
                    (eq y 'Klein)
                    (eq y 'Torus)))
           (integerp (get-topo-left-neighbor x y z))))
  
(defthm get-left-neighbor-delivers-int
  (implies(and (natp x)
               (integerp z)
               (cell-in-range? x z)
                (or (eq y 'Cylinder)
                    (eq y 'Moebius)
                    (eq y 'Klein)
                    (eq y 'Torus)))
          (integerp (get-left-neighbor x y z))))

(defthm get-topo-right-neighbor-delivers-int
  (implies (and (integerp x)
                (integerp z)
                (or (eq y 'Cylinder)
                    (eq y 'Moebius)
                    (eq y 'Klein)
                    (eq y 'Torus)))
           (integerp (get-topo-right-neighbor x y z))))
  
(defthm get-right-neighbor-delivers-int
  (implies(and (natp x)
               (integerp z)
               (cell-in-range? x z)
                (or (eq y 'Cylinder)
                    (eq y 'Moebius)
                    (eq y 'Klein)
                    (eq y 'Torus)))
          (integerp (get-right-neighbor x y z))))

(defthm neighbor-list-deliver-true-list
  (true-listp (neighbor-list x y z)))

(defthm alive?-delivers-boolean
  (booleanp (alive? x y)))

(defthm check-dead-neighbors-delivers-true-list
  (true-listp (check-dead-neighbors x)))

(defthm merge-sort-delivers-list
  (implies (true-listp xs)
           (true-listp (merge-sort xs))))

(defthm merge-sort-by-time-delivers-list
  (implies (true-listp xs)
           (true-listp (merge-sort-by-time xs))))

;;---------------------------------------------------------------------------
;;
;;	The following merge-sort theorems were reprinted from
;;	http://en.literateprograms.org/Merge_sort_(ACL2).
;;
;;---------------------------------------------------------------------------
(defthm mergesort-ordered
  (ordered-p (merge-sort x)))

(defthm rat-list->string-delivers-string
  (stringp (rat-list->string x)))

(defthm permutation-p-reflexive
  (permutation-p x x))

(defthm delete-different-element-preserves-member
  (implies (not (equal a b))
	   (iff (member a (delete-element b x))
		(member a x))))

(defthm permutation-p-implies-member-iff
  (implies (permutation-p x y)
	   (iff (member a x)
		(member a y))))


(defthm delete-element-commutes
  (equal (delete-element a (delete-element b c))
	 (delete-element b (delete-element a c))))

(defthm delete-same-member-preserves-permutation-p
  (implies (and (member x a)
		(member x b)
		(permutation-p a b))
	   (permutation-p (delete-element x a)
			  (delete-element x b))))


(defthm permutation-p-transitive
  (implies (and (permutation-p x y)
		(permutation-p y z))
	   (permutation-p x z)))


(in-theory (disable permutation-p-implies-member-iff))

(defthm cons-delete-permutation-of-original
  (implies (and (member a y)
		(permutation-p (cons a (delete-element a y)) x))
	   (permutation-p y x)))

(defthm permutation-p-symmetric
  (implies (permutation-p x y)
	   (permutation-p y x)))

;(defequiv permutation-p)
(defthm permutation-p-is-an-equivalence
  (and (booleanp (permutation-p x y))
       (permutation-p x x)
       (implies (permutation-p x y) (permutation-p y x))
       (implies (and (permutation-p x y)
                     (permutation-p y z))
                (permutation-p x z)))
  :rule-classes (:equivalence))

;--------------------------------------------------------

; Main lemmas and final result

;--------------------------------------------------------


(defthm permutation-p-implies-permutation-p-append-2
  (implies (permutation-p y y-equiv)
	   (permutation-p (append x y)
			  (append x y-equiv)))
  :rule-classes (:congruence))

(defthm member-of-append-iff-member-of-operand
  (iff (member a (append x y))
       (or (member a x)
	   (member a y))))

(defthm permutation-p-implies-permutation-p-append-1
  (implies (permutation-p x x-equiv)
	   (permutation-p (append x y)
			  (append x-equiv y)))
  :rule-classes (:congruence))

(defthm append-commutative-wrt-permutation
  (permutation-p (append x y)
		 (append y x)))

(defthm permutation-p-implies-permutation-p-delete-2
  (implies (permutation-p x x-equiv)
	   (permutation-p (delete-element a x)
			  (delete-element a x-equiv)))
  :rule-classes (:congruence))

(defthm delete-append-deletes-from-leftmost-containing
  (equal (delete-element a (append x y))
	 (if (member a x)
	     (append (delete-element a x) y)
	   (append x (delete-element a y)))))

;;-----------------------------------------------------------------------------
;;    The following commented-out theorems will not admit.
;;
;;-----------------------------------------------------------------------------

;(defthm merge-results-permutation-of-append
;  (permutation-p (merge-results x y)
;		 (append x y))
;  :hints (("Goal" :induct (merge-results x y))))


;(defthm append-cons-commute-under-permutation
;  (permutation-p (append x (cons a y))
;		 (cons a (append x y))))

;(defthm append-split-permutation-of-original
;  (permutation-p (append (car (split-list x))
;			 (mv-nth 1 (split-list x)))
;		 x))


;(defthm mergesort-permutation-of-input
;  (permutation-p (mergesort x) x))

;(defthm mergesort-correct
;  (and (ordered-p (mergesort x))
;       (permutation-p (mergesort x) x))
;  :rule-classes nil)

;;-----------------------------------------------------------------------------
;;        End Section.
;;
;;-----------------------------------------------------------------------------

(defthm avl-insertion-preserves-membership
  (implies (and (avl-tree? t)
                (key? k)
                (occurs-in-tree? k t))
           (occurs-in-tree? k (avl-insert t x y))))

(defthm avl-deletion-preserves-membership
  (implies (and (avl-tree? t)
                (key? k)
                (occurs-in-tree? k t))
           (occurs-in-tree? k (avl-delete x t))))

(defthm avl-flatten-preserves-membership
  (implies (and (avl-tree? t)
                (key? k)
                (occurs-in-tree? k t))
           (occurs-in-pairs? k (avl-flatten t))))

(defthm sum-list-delivers-integer
  (implies (and (integer-listp xs)
                (integerp y))
           (integerp (sum-list xs y))))

(defthm length-delivers-rational
  (implies (true-listp xs)
           (rationalp (length xs))))

(defthm length-delivers-rational-on-int-list
  (implies (integer-listp xs)
           (rationalp (length xs))))

(defthm sum-list-delivers-integer-particular
  (implies (integer-listp ys)
           (integerp (sum-list ys 0))))

(defthm calculate-mean-delivers-rational
  (implies (and (consp (cdr xs))
                (integer-listp xs))
           (rationalp (calculate-mean xs))))


;;-----------------------------------------------------------------------------
;;          The following theorems will not admit.
;;
;;-----------------------------------------------------------------------------

;(defthm avl-delete-is-ordered
;  (implies (and (avl-tree? x)
;                (key? y))
;           (ordered? (avl-delete x y))))

;(defthm alive-cells-kill-delivers-tree
;  (implies (and (avl-tree? x)
;                (key? y))
;           (avl-tree? (alive-cells-kill x y))))

;(defthm kill-cells-delivers-avl-tree
;  (implies (and (true-listp x)
;           (avl-tree? y))
;           (avl-tree? (kill-cells x y))))

;(defthm alive-cells-insert-delivers-tree
;  (implies (and (avl-tree? x)
;                (key? y))
;           (avl-tree? (alive-cells-insert x y))))

;(defthm revive-cells-delivers-avl-tree
;  (implies (and (true-listp x)
;           (avl-tree? y))
;           (avl-tree? (revive-cells x y))))

;(defthm update-tree-delivers-tree
;  (implies (and (avl-tree? x)
;                (symbolp y))
;           (avl-tree? (update-tree x y))))
